Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

test2(x_0, y) -> True
test2(x_0, y) -> False
append2(l1_2, l2_1) -> match_03(l1_2, l2_1, l1_2)
match_03(l1_2, l2_1, Nil) -> l2_1
match_03(l1_2, l2_1, Cons2(x, l)) -> Cons2(x, append2(l, l2_1))
part2(a_4, l_3) -> match_13(a_4, l_3, l_3)
match_13(a_4, l_3, Nil) -> Pair2(Nil, Nil)
match_13(a_4, l_3, Cons2(x, l')) -> match_25(x, l', a_4, l_3, part2(a_4, l'))
match_25(x, l', a_4, l_3, Pair2(l1, l2)) -> match_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
match_37(l1, l2, x, l', a_4, l_3, False) -> Pair2(Cons2(x, l1), l2)
match_37(l1, l2, x, l', a_4, l_3, True) -> Pair2(l1, Cons2(x, l2))
quick1(l_5) -> match_42(l_5, l_5)
match_42(l_5, Nil) -> Nil
match_42(l_5, Cons2(a, l')) -> match_54(a, l', l_5, part2(a, l'))
match_54(a, l', l_5, Pair2(l1, l2)) -> append2(quick1(l1), Cons2(a, quick1(l2)))

Q is empty.


QTRS
  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

test2(x_0, y) -> True
test2(x_0, y) -> False
append2(l1_2, l2_1) -> match_03(l1_2, l2_1, l1_2)
match_03(l1_2, l2_1, Nil) -> l2_1
match_03(l1_2, l2_1, Cons2(x, l)) -> Cons2(x, append2(l, l2_1))
part2(a_4, l_3) -> match_13(a_4, l_3, l_3)
match_13(a_4, l_3, Nil) -> Pair2(Nil, Nil)
match_13(a_4, l_3, Cons2(x, l')) -> match_25(x, l', a_4, l_3, part2(a_4, l'))
match_25(x, l', a_4, l_3, Pair2(l1, l2)) -> match_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
match_37(l1, l2, x, l', a_4, l_3, False) -> Pair2(Cons2(x, l1), l2)
match_37(l1, l2, x, l', a_4, l_3, True) -> Pair2(l1, Cons2(x, l2))
quick1(l_5) -> match_42(l_5, l_5)
match_42(l_5, Nil) -> Nil
match_42(l_5, Cons2(a, l')) -> match_54(a, l', l_5, part2(a, l'))
match_54(a, l', l_5, Pair2(l1, l2)) -> append2(quick1(l1), Cons2(a, quick1(l2)))

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

MATCH_25(x, l', a_4, l_3, Pair2(l1, l2)) -> TEST2(a_4, x)
MATCH_42(l_5, Cons2(a, l')) -> PART2(a, l')
APPEND2(l1_2, l2_1) -> MATCH_03(l1_2, l2_1, l1_2)
MATCH_13(a_4, l_3, Cons2(x, l')) -> PART2(a_4, l')
MATCH_54(a, l', l_5, Pair2(l1, l2)) -> APPEND2(quick1(l1), Cons2(a, quick1(l2)))
MATCH_54(a, l', l_5, Pair2(l1, l2)) -> QUICK1(l1)
QUICK1(l_5) -> MATCH_42(l_5, l_5)
MATCH_42(l_5, Cons2(a, l')) -> MATCH_54(a, l', l_5, part2(a, l'))
MATCH_03(l1_2, l2_1, Cons2(x, l)) -> APPEND2(l, l2_1)
MATCH_25(x, l', a_4, l_3, Pair2(l1, l2)) -> MATCH_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
MATCH_13(a_4, l_3, Cons2(x, l')) -> MATCH_25(x, l', a_4, l_3, part2(a_4, l'))
PART2(a_4, l_3) -> MATCH_13(a_4, l_3, l_3)
MATCH_54(a, l', l_5, Pair2(l1, l2)) -> QUICK1(l2)

The TRS R consists of the following rules:

test2(x_0, y) -> True
test2(x_0, y) -> False
append2(l1_2, l2_1) -> match_03(l1_2, l2_1, l1_2)
match_03(l1_2, l2_1, Nil) -> l2_1
match_03(l1_2, l2_1, Cons2(x, l)) -> Cons2(x, append2(l, l2_1))
part2(a_4, l_3) -> match_13(a_4, l_3, l_3)
match_13(a_4, l_3, Nil) -> Pair2(Nil, Nil)
match_13(a_4, l_3, Cons2(x, l')) -> match_25(x, l', a_4, l_3, part2(a_4, l'))
match_25(x, l', a_4, l_3, Pair2(l1, l2)) -> match_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
match_37(l1, l2, x, l', a_4, l_3, False) -> Pair2(Cons2(x, l1), l2)
match_37(l1, l2, x, l', a_4, l_3, True) -> Pair2(l1, Cons2(x, l2))
quick1(l_5) -> match_42(l_5, l_5)
match_42(l_5, Nil) -> Nil
match_42(l_5, Cons2(a, l')) -> match_54(a, l', l_5, part2(a, l'))
match_54(a, l', l_5, Pair2(l1, l2)) -> append2(quick1(l1), Cons2(a, quick1(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
QDP
      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

MATCH_25(x, l', a_4, l_3, Pair2(l1, l2)) -> TEST2(a_4, x)
MATCH_42(l_5, Cons2(a, l')) -> PART2(a, l')
APPEND2(l1_2, l2_1) -> MATCH_03(l1_2, l2_1, l1_2)
MATCH_13(a_4, l_3, Cons2(x, l')) -> PART2(a_4, l')
MATCH_54(a, l', l_5, Pair2(l1, l2)) -> APPEND2(quick1(l1), Cons2(a, quick1(l2)))
MATCH_54(a, l', l_5, Pair2(l1, l2)) -> QUICK1(l1)
QUICK1(l_5) -> MATCH_42(l_5, l_5)
MATCH_42(l_5, Cons2(a, l')) -> MATCH_54(a, l', l_5, part2(a, l'))
MATCH_03(l1_2, l2_1, Cons2(x, l)) -> APPEND2(l, l2_1)
MATCH_25(x, l', a_4, l_3, Pair2(l1, l2)) -> MATCH_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
MATCH_13(a_4, l_3, Cons2(x, l')) -> MATCH_25(x, l', a_4, l_3, part2(a_4, l'))
PART2(a_4, l_3) -> MATCH_13(a_4, l_3, l_3)
MATCH_54(a, l', l_5, Pair2(l1, l2)) -> QUICK1(l2)

The TRS R consists of the following rules:

test2(x_0, y) -> True
test2(x_0, y) -> False
append2(l1_2, l2_1) -> match_03(l1_2, l2_1, l1_2)
match_03(l1_2, l2_1, Nil) -> l2_1
match_03(l1_2, l2_1, Cons2(x, l)) -> Cons2(x, append2(l, l2_1))
part2(a_4, l_3) -> match_13(a_4, l_3, l_3)
match_13(a_4, l_3, Nil) -> Pair2(Nil, Nil)
match_13(a_4, l_3, Cons2(x, l')) -> match_25(x, l', a_4, l_3, part2(a_4, l'))
match_25(x, l', a_4, l_3, Pair2(l1, l2)) -> match_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
match_37(l1, l2, x, l', a_4, l_3, False) -> Pair2(Cons2(x, l1), l2)
match_37(l1, l2, x, l', a_4, l_3, True) -> Pair2(l1, Cons2(x, l2))
quick1(l_5) -> match_42(l_5, l_5)
match_42(l_5, Nil) -> Nil
match_42(l_5, Cons2(a, l')) -> match_54(a, l', l_5, part2(a, l'))
match_54(a, l', l_5, Pair2(l1, l2)) -> append2(quick1(l1), Cons2(a, quick1(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 3 SCCs with 5 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
QDP
            ↳ QDPOrderProof
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PART2(a_4, l_3) -> MATCH_13(a_4, l_3, l_3)
MATCH_13(a_4, l_3, Cons2(x, l')) -> PART2(a_4, l')

The TRS R consists of the following rules:

test2(x_0, y) -> True
test2(x_0, y) -> False
append2(l1_2, l2_1) -> match_03(l1_2, l2_1, l1_2)
match_03(l1_2, l2_1, Nil) -> l2_1
match_03(l1_2, l2_1, Cons2(x, l)) -> Cons2(x, append2(l, l2_1))
part2(a_4, l_3) -> match_13(a_4, l_3, l_3)
match_13(a_4, l_3, Nil) -> Pair2(Nil, Nil)
match_13(a_4, l_3, Cons2(x, l')) -> match_25(x, l', a_4, l_3, part2(a_4, l'))
match_25(x, l', a_4, l_3, Pair2(l1, l2)) -> match_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
match_37(l1, l2, x, l', a_4, l_3, False) -> Pair2(Cons2(x, l1), l2)
match_37(l1, l2, x, l', a_4, l_3, True) -> Pair2(l1, Cons2(x, l2))
quick1(l_5) -> match_42(l_5, l_5)
match_42(l_5, Nil) -> Nil
match_42(l_5, Cons2(a, l')) -> match_54(a, l', l_5, part2(a, l'))
match_54(a, l', l_5, Pair2(l1, l2)) -> append2(quick1(l1), Cons2(a, quick1(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


MATCH_13(a_4, l_3, Cons2(x, l')) -> PART2(a_4, l')
The remaining pairs can at least be oriented weakly.

PART2(a_4, l_3) -> MATCH_13(a_4, l_3, l_3)
Used ordering: Polynomial Order [17,21] with Interpretation:

POL( PART2(x1, x2) ) = 2x1 + 2x2 + 2


POL( Cons2(x1, x2) ) = x1 + x2 + 2


POL( MATCH_13(x1, ..., x3) ) = 2x1 + 2x3 + 2



The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
            ↳ QDPOrderProof
QDP
                ↳ DependencyGraphProof
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PART2(a_4, l_3) -> MATCH_13(a_4, l_3, l_3)

The TRS R consists of the following rules:

test2(x_0, y) -> True
test2(x_0, y) -> False
append2(l1_2, l2_1) -> match_03(l1_2, l2_1, l1_2)
match_03(l1_2, l2_1, Nil) -> l2_1
match_03(l1_2, l2_1, Cons2(x, l)) -> Cons2(x, append2(l, l2_1))
part2(a_4, l_3) -> match_13(a_4, l_3, l_3)
match_13(a_4, l_3, Nil) -> Pair2(Nil, Nil)
match_13(a_4, l_3, Cons2(x, l')) -> match_25(x, l', a_4, l_3, part2(a_4, l'))
match_25(x, l', a_4, l_3, Pair2(l1, l2)) -> match_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
match_37(l1, l2, x, l', a_4, l_3, False) -> Pair2(Cons2(x, l1), l2)
match_37(l1, l2, x, l', a_4, l_3, True) -> Pair2(l1, Cons2(x, l2))
quick1(l_5) -> match_42(l_5, l_5)
match_42(l_5, Nil) -> Nil
match_42(l_5, Cons2(a, l')) -> match_54(a, l', l_5, part2(a, l'))
match_54(a, l', l_5, Pair2(l1, l2)) -> append2(quick1(l1), Cons2(a, quick1(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 0 SCCs with 1 less node.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
QDP
            ↳ QDPOrderProof
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MATCH_03(l1_2, l2_1, Cons2(x, l)) -> APPEND2(l, l2_1)
APPEND2(l1_2, l2_1) -> MATCH_03(l1_2, l2_1, l1_2)

The TRS R consists of the following rules:

test2(x_0, y) -> True
test2(x_0, y) -> False
append2(l1_2, l2_1) -> match_03(l1_2, l2_1, l1_2)
match_03(l1_2, l2_1, Nil) -> l2_1
match_03(l1_2, l2_1, Cons2(x, l)) -> Cons2(x, append2(l, l2_1))
part2(a_4, l_3) -> match_13(a_4, l_3, l_3)
match_13(a_4, l_3, Nil) -> Pair2(Nil, Nil)
match_13(a_4, l_3, Cons2(x, l')) -> match_25(x, l', a_4, l_3, part2(a_4, l'))
match_25(x, l', a_4, l_3, Pair2(l1, l2)) -> match_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
match_37(l1, l2, x, l', a_4, l_3, False) -> Pair2(Cons2(x, l1), l2)
match_37(l1, l2, x, l', a_4, l_3, True) -> Pair2(l1, Cons2(x, l2))
quick1(l_5) -> match_42(l_5, l_5)
match_42(l_5, Nil) -> Nil
match_42(l_5, Cons2(a, l')) -> match_54(a, l', l_5, part2(a, l'))
match_54(a, l', l_5, Pair2(l1, l2)) -> append2(quick1(l1), Cons2(a, quick1(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


MATCH_03(l1_2, l2_1, Cons2(x, l)) -> APPEND2(l, l2_1)
The remaining pairs can at least be oriented weakly.

APPEND2(l1_2, l2_1) -> MATCH_03(l1_2, l2_1, l1_2)
Used ordering: Polynomial Order [17,21] with Interpretation:

POL( Cons2(x1, x2) ) = 2x1 + x2 + 1


POL( APPEND2(x1, x2) ) = 2x1 + 2x2


POL( MATCH_03(x1, ..., x3) ) = max{0, 2x2 + 2x3 - 1}



The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
QDP
                ↳ DependencyGraphProof
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APPEND2(l1_2, l2_1) -> MATCH_03(l1_2, l2_1, l1_2)

The TRS R consists of the following rules:

test2(x_0, y) -> True
test2(x_0, y) -> False
append2(l1_2, l2_1) -> match_03(l1_2, l2_1, l1_2)
match_03(l1_2, l2_1, Nil) -> l2_1
match_03(l1_2, l2_1, Cons2(x, l)) -> Cons2(x, append2(l, l2_1))
part2(a_4, l_3) -> match_13(a_4, l_3, l_3)
match_13(a_4, l_3, Nil) -> Pair2(Nil, Nil)
match_13(a_4, l_3, Cons2(x, l')) -> match_25(x, l', a_4, l_3, part2(a_4, l'))
match_25(x, l', a_4, l_3, Pair2(l1, l2)) -> match_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
match_37(l1, l2, x, l', a_4, l_3, False) -> Pair2(Cons2(x, l1), l2)
match_37(l1, l2, x, l', a_4, l_3, True) -> Pair2(l1, Cons2(x, l2))
quick1(l_5) -> match_42(l_5, l_5)
match_42(l_5, Nil) -> Nil
match_42(l_5, Cons2(a, l')) -> match_54(a, l', l_5, part2(a, l'))
match_54(a, l', l_5, Pair2(l1, l2)) -> append2(quick1(l1), Cons2(a, quick1(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 0 SCCs with 1 less node.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
QDP
            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

MATCH_42(l_5, Cons2(a, l')) -> MATCH_54(a, l', l_5, part2(a, l'))
QUICK1(l_5) -> MATCH_42(l_5, l_5)
MATCH_54(a, l', l_5, Pair2(l1, l2)) -> QUICK1(l2)
MATCH_54(a, l', l_5, Pair2(l1, l2)) -> QUICK1(l1)

The TRS R consists of the following rules:

test2(x_0, y) -> True
test2(x_0, y) -> False
append2(l1_2, l2_1) -> match_03(l1_2, l2_1, l1_2)
match_03(l1_2, l2_1, Nil) -> l2_1
match_03(l1_2, l2_1, Cons2(x, l)) -> Cons2(x, append2(l, l2_1))
part2(a_4, l_3) -> match_13(a_4, l_3, l_3)
match_13(a_4, l_3, Nil) -> Pair2(Nil, Nil)
match_13(a_4, l_3, Cons2(x, l')) -> match_25(x, l', a_4, l_3, part2(a_4, l'))
match_25(x, l', a_4, l_3, Pair2(l1, l2)) -> match_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
match_37(l1, l2, x, l', a_4, l_3, False) -> Pair2(Cons2(x, l1), l2)
match_37(l1, l2, x, l', a_4, l_3, True) -> Pair2(l1, Cons2(x, l2))
quick1(l_5) -> match_42(l_5, l_5)
match_42(l_5, Nil) -> Nil
match_42(l_5, Cons2(a, l')) -> match_54(a, l', l_5, part2(a, l'))
match_54(a, l', l_5, Pair2(l1, l2)) -> append2(quick1(l1), Cons2(a, quick1(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


MATCH_42(l_5, Cons2(a, l')) -> MATCH_54(a, l', l_5, part2(a, l'))
The remaining pairs can at least be oriented weakly.

QUICK1(l_5) -> MATCH_42(l_5, l_5)
MATCH_54(a, l', l_5, Pair2(l1, l2)) -> QUICK1(l2)
MATCH_54(a, l', l_5, Pair2(l1, l2)) -> QUICK1(l1)
Used ordering: Polynomial Order [17,21] with Interpretation:

POL( Nil ) = max{0, -1}


POL( part2(x1, x2) ) = x2


POL( False ) = 2


POL( QUICK1(x1) ) = x1


POL( match_25(x1, ..., x5) ) = x5 + 2


POL( match_37(x1, ..., x7) ) = x1 + x2 + 1


POL( test2(x1, x2) ) = max{0, 2x1 + 2x2 - 2}


POL( Cons2(x1, x2) ) = x2 + 2


POL( MATCH_54(x1, ..., x4) ) = x4 + 1


POL( match_13(x1, ..., x3) ) = x3


POL( True ) = max{0, -2}


POL( MATCH_42(x1, x2) ) = x2


POL( Pair2(x1, x2) ) = max{0, x1 + x2 - 1}



The following usable rules [14] were oriented:

match_13(a_4, l_3, Nil) -> Pair2(Nil, Nil)
part2(a_4, l_3) -> match_13(a_4, l_3, l_3)
match_37(l1, l2, x, l', a_4, l_3, True) -> Pair2(l1, Cons2(x, l2))
match_25(x, l', a_4, l_3, Pair2(l1, l2)) -> match_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
match_13(a_4, l_3, Cons2(x, l')) -> match_25(x, l', a_4, l_3, part2(a_4, l'))
match_37(l1, l2, x, l', a_4, l_3, False) -> Pair2(Cons2(x, l1), l2)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
QDP
                ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

QUICK1(l_5) -> MATCH_42(l_5, l_5)
MATCH_54(a, l', l_5, Pair2(l1, l2)) -> QUICK1(l2)
MATCH_54(a, l', l_5, Pair2(l1, l2)) -> QUICK1(l1)

The TRS R consists of the following rules:

test2(x_0, y) -> True
test2(x_0, y) -> False
append2(l1_2, l2_1) -> match_03(l1_2, l2_1, l1_2)
match_03(l1_2, l2_1, Nil) -> l2_1
match_03(l1_2, l2_1, Cons2(x, l)) -> Cons2(x, append2(l, l2_1))
part2(a_4, l_3) -> match_13(a_4, l_3, l_3)
match_13(a_4, l_3, Nil) -> Pair2(Nil, Nil)
match_13(a_4, l_3, Cons2(x, l')) -> match_25(x, l', a_4, l_3, part2(a_4, l'))
match_25(x, l', a_4, l_3, Pair2(l1, l2)) -> match_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
match_37(l1, l2, x, l', a_4, l_3, False) -> Pair2(Cons2(x, l1), l2)
match_37(l1, l2, x, l', a_4, l_3, True) -> Pair2(l1, Cons2(x, l2))
quick1(l_5) -> match_42(l_5, l_5)
match_42(l_5, Nil) -> Nil
match_42(l_5, Cons2(a, l')) -> match_54(a, l', l_5, part2(a, l'))
match_54(a, l', l_5, Pair2(l1, l2)) -> append2(quick1(l1), Cons2(a, quick1(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 0 SCCs with 3 less nodes.